Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ACTIVE(f(X)) → G(X)
SEL(mark(X1), X2) → SEL(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
SEL(X1, active(X2)) → SEL(X1, X2)
MARK(s(X)) → MARK(X)
ACTIVE(g(0)) → MARK(s(0))
ACTIVE(f(X)) → CONS(X, f(g(X)))
MARK(cons(X1, X2)) → MARK(X1)
CONS(X1, mark(X2)) → CONS(X1, X2)
ACTIVE(f(X)) → F(g(X))
ACTIVE(f(X)) → MARK(cons(X, f(g(X))))
MARK(g(X)) → MARK(X)
CONS(X1, active(X2)) → CONS(X1, X2)
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(s(X)) → ACTIVE(s(mark(X)))
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(active(X1), X2) → SEL(X1, X2)
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
F(active(X)) → F(X)
MARK(f(X)) → MARK(X)
F(mark(X)) → F(X)
S(active(X)) → S(X)
S(mark(X)) → S(X)
MARK(sel(X1, X2)) → MARK(X1)
MARK(s(X)) → S(mark(X))
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(g(s(X))) → MARK(s(s(g(X))))
ACTIVE(g(s(X))) → G(X)
MARK(g(X)) → ACTIVE(g(mark(X)))
G(active(X)) → G(X)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
G(mark(X)) → G(X)
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(g(X)) → G(mark(X))
ACTIVE(g(0)) → S(0)
MARK(sel(X1, X2)) → SEL(mark(X1), mark(X2))
MARK(0) → ACTIVE(0)
MARK(f(X)) → F(mark(X))
CONS(active(X1), X2) → CONS(X1, X2)
ACTIVE(g(s(X))) → S(g(X))
ACTIVE(sel(s(X), cons(Y, Z))) → SEL(X, Z)
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(g(s(X))) → S(s(g(X)))

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(f(X)) → G(X)
SEL(mark(X1), X2) → SEL(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
SEL(X1, active(X2)) → SEL(X1, X2)
MARK(s(X)) → MARK(X)
ACTIVE(g(0)) → MARK(s(0))
ACTIVE(f(X)) → CONS(X, f(g(X)))
MARK(cons(X1, X2)) → MARK(X1)
CONS(X1, mark(X2)) → CONS(X1, X2)
ACTIVE(f(X)) → F(g(X))
ACTIVE(f(X)) → MARK(cons(X, f(g(X))))
MARK(g(X)) → MARK(X)
CONS(X1, active(X2)) → CONS(X1, X2)
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(s(X)) → ACTIVE(s(mark(X)))
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(active(X1), X2) → SEL(X1, X2)
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
F(active(X)) → F(X)
MARK(f(X)) → MARK(X)
F(mark(X)) → F(X)
S(active(X)) → S(X)
S(mark(X)) → S(X)
MARK(sel(X1, X2)) → MARK(X1)
MARK(s(X)) → S(mark(X))
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(g(s(X))) → MARK(s(s(g(X))))
ACTIVE(g(s(X))) → G(X)
MARK(g(X)) → ACTIVE(g(mark(X)))
G(active(X)) → G(X)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
G(mark(X)) → G(X)
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(g(X)) → G(mark(X))
ACTIVE(g(0)) → S(0)
MARK(sel(X1, X2)) → SEL(mark(X1), mark(X2))
MARK(0) → ACTIVE(0)
MARK(f(X)) → F(mark(X))
CONS(active(X1), X2) → CONS(X1, X2)
ACTIVE(g(s(X))) → S(g(X))
ACTIVE(sel(s(X), cons(Y, Z))) → SEL(X, Z)
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(g(s(X))) → S(s(g(X)))

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 6 SCCs with 14 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SEL(mark(X1), X2) → SEL(X1, X2)
SEL(X1, active(X2)) → SEL(X1, X2)
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(active(X1), X2) → SEL(X1, X2)

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SEL(mark(X1), X2) → SEL(X1, X2)
SEL(X1, active(X2)) → SEL(X1, X2)
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(active(X1), X2) → SEL(X1, X2)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(mark(X)) → S(X)
S(active(X)) → S(X)

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(active(X)) → S(X)
S(mark(X)) → S(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

G(active(X)) → G(X)
G(mark(X)) → G(X)

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

G(active(X)) → G(X)
G(mark(X)) → G(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONS(X1, active(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONS(mark(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(mark(X)) → F(X)
F(active(X)) → F(X)

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(mark(X)) → F(X)
F(active(X)) → F(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(sel(X1, X2)) → MARK(X1)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(s(X)) → MARK(X)
ACTIVE(g(0)) → MARK(s(0))
ACTIVE(g(s(X))) → MARK(s(s(g(X))))
MARK(cons(X1, X2)) → MARK(X1)
MARK(g(X)) → ACTIVE(g(mark(X)))
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
MARK(f(X)) → ACTIVE(f(mark(X)))
ACTIVE(f(X)) → MARK(cons(X, f(g(X))))
MARK(g(X)) → MARK(X)
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(s(X)) → ACTIVE(s(mark(X)))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
MARK(sel(X1, X2)) → MARK(X2)
MARK(f(X)) → MARK(X)

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(s(X)) → ACTIVE(s(mark(X)))
The remaining pairs can at least be oriented weakly.

MARK(sel(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
ACTIVE(g(0)) → MARK(s(0))
ACTIVE(g(s(X))) → MARK(s(s(g(X))))
MARK(cons(X1, X2)) → MARK(X1)
MARK(g(X)) → ACTIVE(g(mark(X)))
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
MARK(f(X)) → ACTIVE(f(mark(X)))
ACTIVE(f(X)) → MARK(cons(X, f(g(X))))
MARK(g(X)) → MARK(X)
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
MARK(sel(X1, X2)) → MARK(X2)
MARK(f(X)) → MARK(X)
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(ACTIVE(x1)) = x1   
POL(MARK(x1)) = 1   
POL(active(x1)) = 0   
POL(cons(x1, x2)) = 0   
POL(f(x1)) = 1   
POL(g(x1)) = 1   
POL(mark(x1)) = 0   
POL(s(x1)) = 0   
POL(sel(x1, x2)) = 1   

The following usable rules [17] were oriented:

f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
s(active(X)) → s(X)
s(mark(X)) → s(X)
sel(X1, mark(X2)) → sel(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
g(active(X)) → g(X)
g(mark(X)) → g(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(sel(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
ACTIVE(g(0)) → MARK(s(0))
ACTIVE(g(s(X))) → MARK(s(s(g(X))))
MARK(cons(X1, X2)) → MARK(X1)
MARK(g(X)) → ACTIVE(g(mark(X)))
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
MARK(f(X)) → ACTIVE(f(mark(X)))
ACTIVE(f(X)) → MARK(cons(X, f(g(X))))
MARK(g(X)) → MARK(X)
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
MARK(sel(X1, X2)) → MARK(X2)
MARK(f(X)) → MARK(X)

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(g(X)) → ACTIVE(g(mark(X))) at position [0] we obtained the following new rules:

MARK(g(f(x0))) → ACTIVE(g(active(f(mark(x0)))))
MARK(g(sel(x0, x1))) → ACTIVE(g(active(sel(mark(x0), mark(x1)))))
MARK(g(s(x0))) → ACTIVE(g(active(s(mark(x0)))))
MARK(g(cons(x0, x1))) → ACTIVE(g(active(cons(mark(x0), x1))))
MARK(g(x0)) → ACTIVE(g(x0))
MARK(g(g(x0))) → ACTIVE(g(active(g(mark(x0)))))
MARK(g(0)) → ACTIVE(g(active(0)))



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(g(sel(x0, x1))) → ACTIVE(g(active(sel(mark(x0), mark(x1)))))
MARK(sel(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
ACTIVE(g(s(X))) → MARK(s(s(g(X))))
ACTIVE(g(0)) → MARK(s(0))
MARK(cons(X1, X2)) → MARK(X1)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
MARK(g(X)) → MARK(X)
ACTIVE(f(X)) → MARK(cons(X, f(g(X))))
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(g(f(x0))) → ACTIVE(g(active(f(mark(x0)))))
MARK(g(s(x0))) → ACTIVE(g(active(s(mark(x0)))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(g(cons(x0, x1))) → ACTIVE(g(active(cons(mark(x0), x1))))
MARK(g(x0)) → ACTIVE(g(x0))
MARK(g(g(x0))) → ACTIVE(g(active(g(mark(x0)))))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
MARK(g(0)) → ACTIVE(g(active(0)))
MARK(sel(X1, X2)) → MARK(X2)
MARK(f(X)) → MARK(X)

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2))) at position [0] we obtained the following new rules:

MARK(sel(y0, f(x0))) → ACTIVE(sel(mark(y0), active(f(mark(x0)))))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(mark(x0), x1)), mark(y1)))
MARK(sel(g(x0), y1)) → ACTIVE(sel(active(g(mark(x0))), mark(y1)))
MARK(sel(f(x0), y1)) → ACTIVE(sel(active(f(mark(x0))), mark(y1)))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(mark(x0), x1))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(sel(y0, g(x0))) → ACTIVE(sel(mark(y0), active(g(mark(x0)))))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(mark(x0)))))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(mark(x0))), mark(y1)))



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ SemLabProof
                        ↳ SemLabProof2

Q DP problem:
The TRS P consists of the following rules:

MARK(sel(y0, f(x0))) → ACTIVE(sel(mark(y0), active(f(mark(x0)))))
MARK(s(X)) → MARK(X)
ACTIVE(g(0)) → MARK(s(0))
MARK(cons(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(mark(x0), x1)), mark(y1)))
MARK(g(X)) → MARK(X)
ACTIVE(f(X)) → MARK(cons(X, f(g(X))))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(g(f(x0))) → ACTIVE(g(active(f(mark(x0)))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(mark(x0), x1))))
MARK(g(cons(x0, x1))) → ACTIVE(g(active(cons(mark(x0), x1))))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(g(g(x0))) → ACTIVE(g(active(g(mark(x0)))))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(mark(x0)))))
MARK(f(X)) → MARK(X)
MARK(g(sel(x0, x1))) → ACTIVE(g(active(sel(mark(x0), mark(x1)))))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
ACTIVE(g(s(X))) → MARK(s(s(g(X))))
MARK(sel(g(x0), y1)) → ACTIVE(sel(active(g(mark(x0))), mark(y1)))
MARK(sel(f(x0), y1)) → ACTIVE(sel(active(f(mark(x0))), mark(y1)))
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(g(s(x0))) → ACTIVE(g(active(s(mark(x0)))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, g(x0))) → ACTIVE(sel(mark(y0), active(g(mark(x0)))))
MARK(g(x0)) → ACTIVE(g(x0))
MARK(g(0)) → ACTIVE(g(active(0)))
MARK(sel(X1, X2)) → MARK(X2)
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(mark(x0))), mark(y1)))

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We found the following model for the rules of the TRS R. Interpretation over the domain with elements from 0 to 1.sel: 0
cons: 0
active: 0
f: 0
MARK: 0
g: 0
mark: 0
s: 0
0: 1
ACTIVE: 0
By semantic labelling [33] we obtain the following labelled TRS:Q DP problem:
The TRS P consists of the following rules:

MARK.0(g.0(f.0(x0))) → ACTIVE.0(g.0(active.0(f.0(mark.0(x0)))))
MARK.0(f.0(X)) → MARK.0(X)
ACTIVE.0(sel.0-0(s.1(X), cons.0-1(Y, Z))) → MARK.0(sel.1-1(X, Z))
MARK.0(sel.1-0(x0, y1)) → ACTIVE.0(sel.1-0(x0, mark.0(y1)))
MARK.0(sel.0-0(y0, cons.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-1(mark.0(x0), x1))))
MARK.0(sel.0-1(cons.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.1(x0), x1)), mark.1(y1)))
MARK.0(sel.1-0(y0, f.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(f.0(mark.0(x0)))))
MARK.0(sel.1-1(X1, X2)) → MARK.1(X1)
MARK.0(sel.1-0(X1, X2)) → MARK.1(X1)
MARK.0(sel.0-0(cons.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.1(x0), x1)), mark.0(y1)))
MARK.0(sel.1-0(y0, cons.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-0(mark.0(x0), x1))))
ACTIVE.0(sel.0-0(s.1(X), cons.0-0(Y, Z))) → MARK.0(sel.1-0(X, Z))
MARK.0(g.0(x0)) → ACTIVE.0(g.0(x0))
MARK.0(sel.0-0(cons.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.1(x0), x1)), mark.0(y1)))
ACTIVE.0(sel.1-0(0., cons.0-1(X, Y))) → MARK.0(X)
MARK.0(sel.0-1(f.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.0(x0))), mark.1(y1)))
MARK.0(sel.0-1(x0, y1)) → ACTIVE.0(sel.0-0(x0, mark.1(y1)))
MARK.0(sel.0-0(sel.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.0(x1))), mark.0(y1)))
MARK.0(sel.0-0(y0, sel.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.0-0(f.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.0(x0))), mark.0(y1)))
MARK.0(sel.0-0(sel.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.0(x1))), mark.0(y1)))
MARK.0(sel.0-0(sel.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.1(x1))), mark.0(y1)))
MARK.0(g.0(f.1(x0))) → ACTIVE.0(g.0(active.0(f.0(mark.1(x0)))))
MARK.0(sel.1-1(0., y1)) → ACTIVE.0(sel.0-0(active.1(0.), mark.1(y1)))
MARK.0(sel.1-1(y0, 0.)) → ACTIVE.0(sel.0-0(mark.1(y0), active.1(0.)))
MARK.0(sel.0-0(y0, f.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(f.0(mark.1(x0)))))
MARK.0(sel.0-0(y0, cons.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-0(mark.1(x0), x1))))
MARK.0(g.0(s.1(x0))) → ACTIVE.0(g.0(active.0(s.0(mark.1(x0)))))
MARK.0(g.0(cons.1-1(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(sel.0-1(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.0-0(g.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.0-0(y0, g.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(g.0(mark.1(x0)))))
MARK.0(sel.0-1(s.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.0(x0))), mark.1(y1)))
MARK.0(f.1(X)) → MARK.1(X)
MARK.0(sel.0-1(cons.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.1(x0), x1)), mark.1(y1)))
MARK.0(sel.0-1(X1, X2)) → MARK.0(X1)
ACTIVE.0(sel.0-0(s.0(X), cons.0-0(Y, Z))) → MARK.0(sel.0-0(X, Z))
MARK.0(sel.0-0(s.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.0(x0))), mark.0(y1)))
MARK.0(sel.0-0(y0, sel.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(g.0(sel.1-1(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.0-1(y0, x1)) → ACTIVE.0(sel.0-1(mark.0(y0), x1))
MARK.0(sel.0-1(f.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.1-0(y0, cons.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-0(mark.1(x0), x1))))
MARK.0(sel.0-1(g.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.0(x0))), mark.1(y1)))
ACTIVE.0(g.0(s.0(X))) → MARK.0(s.0(s.0(g.0(X))))
MARK.0(sel.0-0(y0, g.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(g.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.0(x0), x1)), mark.0(y1)))
MARK.0(sel.0-0(g.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.0(x0))), mark.0(y1)))
ACTIVE.0(g.0(s.1(X))) → MARK.0(s.0(s.0(g.1(X))))
MARK.0(g.1(X)) → MARK.1(X)
MARK.0(sel.1-0(y0, s.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(s.0(mark.0(x0)))))
MARK.0(sel.0-1(g.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.1(x0))), mark.1(y1)))
MARK.0(g.0(sel.0-0(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(sel.0-0(y0, cons.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(g.1(x0))) → ACTIVE.0(g.0(active.0(g.0(mark.1(x0)))))
MARK.0(sel.0-0(x0, y1)) → ACTIVE.0(sel.0-0(x0, mark.0(y1)))
MARK.0(sel.0-0(y0, x1)) → ACTIVE.0(sel.0-0(mark.0(y0), x1))
ACTIVE.0(sel.1-0(0., cons.0-0(X, Y))) → MARK.0(X)
MARK.0(sel.0-1(sel.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.1(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.1-0(Y, Z))) → MARK.0(sel.1-0(X, Z))
MARK.0(f.1(X)) → ACTIVE.0(f.0(mark.1(X)))
MARK.0(g.0(sel.1-0(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(sel.0-1(sel.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.0(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.1-1(Y, Z))) → MARK.0(sel.1-1(X, Z))
MARK.0(sel.1-0(y0, sel.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, x1)) → ACTIVE.0(sel.0-0(mark.1(y0), x1))
MARK.0(sel.0-0(y0, sel.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(sel.1-0(y0, cons.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-1(mark.0(x0), x1))))
MARK.0(sel.1-0(y0, sel.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(g.0(cons.1-0(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-0(mark.1(x0), x1))))
ACTIVE.0(sel.1-0(0., cons.1-1(X, Y))) → MARK.1(X)
ACTIVE.0(f.1(X)) → MARK.0(cons.1-0(X, f.0(g.1(X))))
ACTIVE.0(f.0(X)) → MARK.0(cons.0-0(X, f.0(g.0(X))))
MARK.0(sel.0-0(y0, s.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(s.0(mark.1(x0)))))
MARK.0(g.0(g.0(x0))) → ACTIVE.0(g.0(active.0(g.0(mark.0(x0)))))
MARK.0(sel.1-0(y0, g.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(g.0(mark.1(x0)))))
MARK.0(cons.0-0(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-1(cons.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.0(x0), x1)), mark.1(y1)))
MARK.0(sel.0-0(f.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.1-1(x0, y1)) → ACTIVE.0(sel.1-0(x0, mark.1(y1)))
MARK.0(sel.1-0(y0, sel.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(s.1(X)) → MARK.1(X)
MARK.0(sel.1-0(y0, sel.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, f.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(f.0(mark.1(x0)))))
MARK.0(sel.0-1(cons.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.0(x0), x1)), mark.1(y1)))
MARK.0(g.1(0.)) → ACTIVE.0(g.0(active.1(0.)))
MARK.0(sel.0-1(X1, X2)) → MARK.1(X2)
MARK.0(sel.0-1(sel.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.0(x1))), mark.1(y1)))
MARK.0(g.0(cons.0-0(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-0(mark.0(x0), x1))))
MARK.0(sel.0-0(cons.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.0(x0), x1)), mark.0(y1)))
MARK.0(sel.1-0(y0, g.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(g.0(mark.0(x0)))))
MARK.0(sel.0-0(s.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.1(x0))), mark.0(y1)))
MARK.0(cons.0-1(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-1(y0, 0.)) → ACTIVE.0(sel.0-0(mark.0(y0), active.1(0.)))
MARK.0(sel.0-0(y0, f.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(f.0(mark.0(x0)))))
MARK.0(g.0(X)) → MARK.0(X)
MARK.0(g.0(s.0(x0))) → ACTIVE.0(g.0(active.0(s.0(mark.0(x0)))))
MARK.0(sel.0-0(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-0(X1, X2)) → MARK.0(X2)
ACTIVE.0(sel.1-0(0., cons.1-0(X, Y))) → MARK.1(X)
ACTIVE.0(sel.0-0(s.0(X), cons.1-1(Y, Z))) → MARK.0(sel.0-1(X, Z))
MARK.0(sel.0-0(y0, s.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(s.0(mark.0(x0)))))
MARK.0(f.0(X)) → ACTIVE.0(f.0(mark.0(X)))
MARK.0(sel.0-0(sel.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.1(x1))), mark.0(y1)))
MARK.0(sel.1-0(y0, s.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(s.0(mark.1(x0)))))
MARK.0(cons.1-1(X1, X2)) → MARK.1(X1)
MARK.0(cons.1-0(X1, X2)) → MARK.1(X1)
ACTIVE.0(g.1(0.)) → MARK.0(s.1(0.))
MARK.0(sel.0-1(s.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.0-0(y0, sel.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(X1, X2)) → MARK.0(X2)
MARK.0(sel.0-1(sel.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.1(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.0(X), cons.1-0(Y, Z))) → MARK.0(sel.0-0(X, Z))
ACTIVE.0(sel.0-0(s.0(X), cons.0-1(Y, Z))) → MARK.0(sel.0-1(X, Z))
MARK.0(sel.0-0(y0, cons.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-0(mark.0(x0), x1))))
MARK.0(g.1(x0)) → ACTIVE.0(g.1(x0))
MARK.0(sel.1-1(y0, x1)) → ACTIVE.0(sel.0-1(mark.1(y0), x1))
MARK.0(sel.1-1(X1, X2)) → MARK.1(X2)
MARK.0(sel.1-0(0., y1)) → ACTIVE.0(sel.0-0(active.1(0.), mark.0(y1)))
MARK.0(s.0(X)) → MARK.0(X)
MARK.0(sel.1-0(y0, cons.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(cons.0-1(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-1(mark.0(x0), x1))))

The TRS R consists of the following rules:

sel.0-1(active.1(X1), X2) → sel.1-1(X1, X2)
mark.0(sel.1-1(X1, X2)) → active.0(sel.0-0(mark.1(X1), mark.1(X2)))
cons.1-0(X1, active.0(X2)) → cons.1-0(X1, X2)
mark.0(cons.1-1(X1, X2)) → active.0(cons.0-1(mark.1(X1), X2))
g.0(active.0(X)) → g.0(X)
cons.0-0(X1, active.1(X2)) → cons.0-1(X1, X2)
active.0(f.1(X)) → mark.0(cons.1-0(X, f.0(g.1(X))))
cons.0-1(active.0(X1), X2) → cons.0-1(X1, X2)
active.0(sel.0-0(s.0(X), cons.1-0(Y, Z))) → mark.0(sel.0-0(X, Z))
sel.1-0(X1, active.1(X2)) → sel.1-1(X1, X2)
cons.0-0(X1, mark.1(X2)) → cons.0-1(X1, X2)
sel.0-1(active.0(X1), X2) → sel.0-1(X1, X2)
cons.1-0(X1, active.1(X2)) → cons.1-1(X1, X2)
cons.0-0(active.0(X1), X2) → cons.0-0(X1, X2)
mark.0(cons.0-1(X1, X2)) → active.0(cons.0-1(mark.0(X1), X2))
mark.0(sel.0-0(X1, X2)) → active.0(sel.0-0(mark.0(X1), mark.0(X2)))
mark.0(s.0(X)) → active.0(s.0(mark.0(X)))
active.0(sel.0-0(s.1(X), cons.1-0(Y, Z))) → mark.0(sel.1-0(X, Z))
mark.0(f.1(X)) → active.0(f.0(mark.1(X)))
sel.0-0(mark.1(X1), X2) → sel.1-0(X1, X2)
sel.0-0(X1, mark.0(X2)) → sel.0-0(X1, X2)
cons.0-1(mark.0(X1), X2) → cons.0-1(X1, X2)
cons.0-0(X1, mark.0(X2)) → cons.0-0(X1, X2)
sel.0-0(X1, mark.1(X2)) → sel.0-1(X1, X2)
cons.0-0(active.1(X1), X2) → cons.1-0(X1, X2)
active.0(sel.0-0(s.1(X), cons.1-1(Y, Z))) → mark.0(sel.1-1(X, Z))
f.0(mark.0(X)) → f.0(X)
f.0(active.1(X)) → f.1(X)
g.0(mark.0(X)) → g.0(X)
cons.1-0(X1, mark.0(X2)) → cons.1-0(X1, X2)
active.0(g.0(s.1(X))) → mark.0(s.0(s.0(g.1(X))))
sel.0-1(mark.1(X1), X2) → sel.1-1(X1, X2)
active.0(sel.0-0(s.0(X), cons.0-1(Y, Z))) → mark.0(sel.0-1(X, Z))
cons.0-0(X1, active.0(X2)) → cons.0-0(X1, X2)
mark.0(s.1(X)) → active.0(s.0(mark.1(X)))
active.0(sel.1-0(0., cons.1-0(X, Y))) → mark.1(X)
mark.0(cons.0-0(X1, X2)) → active.0(cons.0-0(mark.0(X1), X2))
cons.1-0(X1, mark.1(X2)) → cons.1-1(X1, X2)
sel.0-1(mark.0(X1), X2) → sel.0-1(X1, X2)
mark.1(0.) → active.1(0.)
active.0(sel.0-0(s.1(X), cons.0-1(Y, Z))) → mark.0(sel.1-1(X, Z))
sel.1-0(X1, active.0(X2)) → sel.1-0(X1, X2)
active.0(g.0(s.0(X))) → mark.0(s.0(s.0(g.0(X))))
sel.0-0(active.0(X1), X2) → sel.0-0(X1, X2)
cons.0-1(mark.1(X1), X2) → cons.1-1(X1, X2)
sel.0-0(X1, active.0(X2)) → sel.0-0(X1, X2)
s.0(active.0(X)) → s.0(X)
sel.0-0(active.1(X1), X2) → sel.1-0(X1, X2)
cons.0-1(active.1(X1), X2) → cons.1-1(X1, X2)
mark.0(g.1(X)) → active.0(g.0(mark.1(X)))
f.0(active.0(X)) → f.0(X)
s.0(mark.1(X)) → s.1(X)
sel.0-0(mark.0(X1), X2) → sel.0-0(X1, X2)
active.0(sel.0-0(s.1(X), cons.0-0(Y, Z))) → mark.0(sel.1-0(X, Z))
active.0(sel.0-0(s.0(X), cons.0-0(Y, Z))) → mark.0(sel.0-0(X, Z))
sel.1-0(X1, mark.0(X2)) → sel.1-0(X1, X2)
active.0(sel.1-0(0., cons.0-0(X, Y))) → mark.0(X)
active.0(g.1(0.)) → mark.0(s.1(0.))
sel.0-0(X1, active.1(X2)) → sel.0-1(X1, X2)
g.0(active.1(X)) → g.1(X)
mark.0(sel.1-0(X1, X2)) → active.0(sel.0-0(mark.1(X1), mark.0(X2)))
s.0(active.1(X)) → s.1(X)
mark.0(f.0(X)) → active.0(f.0(mark.0(X)))
active.0(sel.0-0(s.0(X), cons.1-1(Y, Z))) → mark.0(sel.0-1(X, Z))
cons.0-0(mark.1(X1), X2) → cons.1-0(X1, X2)
sel.1-0(X1, mark.1(X2)) → sel.1-1(X1, X2)
mark.0(cons.1-0(X1, X2)) → active.0(cons.0-0(mark.1(X1), X2))
active.0(sel.1-0(0., cons.0-1(X, Y))) → mark.0(X)
mark.0(g.0(X)) → active.0(g.0(mark.0(X)))
g.0(mark.1(X)) → g.1(X)
s.0(mark.0(X)) → s.0(X)
f.0(mark.1(X)) → f.1(X)
active.0(f.0(X)) → mark.0(cons.0-0(X, f.0(g.0(X))))
active.0(sel.1-0(0., cons.1-1(X, Y))) → mark.1(X)
cons.0-0(mark.0(X1), X2) → cons.0-0(X1, X2)
mark.0(sel.0-1(X1, X2)) → active.0(sel.0-0(mark.0(X1), mark.1(X2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ SemLabProof
                          ↳ QDP
                            ↳ DependencyGraphProof
                        ↳ SemLabProof2

Q DP problem:
The TRS P consists of the following rules:

MARK.0(g.0(f.0(x0))) → ACTIVE.0(g.0(active.0(f.0(mark.0(x0)))))
MARK.0(f.0(X)) → MARK.0(X)
ACTIVE.0(sel.0-0(s.1(X), cons.0-1(Y, Z))) → MARK.0(sel.1-1(X, Z))
MARK.0(sel.1-0(x0, y1)) → ACTIVE.0(sel.1-0(x0, mark.0(y1)))
MARK.0(sel.0-0(y0, cons.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-1(mark.0(x0), x1))))
MARK.0(sel.0-1(cons.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.1(x0), x1)), mark.1(y1)))
MARK.0(sel.1-0(y0, f.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(f.0(mark.0(x0)))))
MARK.0(sel.1-1(X1, X2)) → MARK.1(X1)
MARK.0(sel.1-0(X1, X2)) → MARK.1(X1)
MARK.0(sel.0-0(cons.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.1(x0), x1)), mark.0(y1)))
MARK.0(sel.1-0(y0, cons.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-0(mark.0(x0), x1))))
ACTIVE.0(sel.0-0(s.1(X), cons.0-0(Y, Z))) → MARK.0(sel.1-0(X, Z))
MARK.0(g.0(x0)) → ACTIVE.0(g.0(x0))
MARK.0(sel.0-0(cons.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.1(x0), x1)), mark.0(y1)))
ACTIVE.0(sel.1-0(0., cons.0-1(X, Y))) → MARK.0(X)
MARK.0(sel.0-1(f.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.0(x0))), mark.1(y1)))
MARK.0(sel.0-1(x0, y1)) → ACTIVE.0(sel.0-0(x0, mark.1(y1)))
MARK.0(sel.0-0(sel.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.0(x1))), mark.0(y1)))
MARK.0(sel.0-0(y0, sel.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.0-0(f.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.0(x0))), mark.0(y1)))
MARK.0(sel.0-0(sel.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.0(x1))), mark.0(y1)))
MARK.0(sel.0-0(sel.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.1(x1))), mark.0(y1)))
MARK.0(g.0(f.1(x0))) → ACTIVE.0(g.0(active.0(f.0(mark.1(x0)))))
MARK.0(sel.1-1(0., y1)) → ACTIVE.0(sel.0-0(active.1(0.), mark.1(y1)))
MARK.0(sel.1-1(y0, 0.)) → ACTIVE.0(sel.0-0(mark.1(y0), active.1(0.)))
MARK.0(sel.0-0(y0, f.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(f.0(mark.1(x0)))))
MARK.0(sel.0-0(y0, cons.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-0(mark.1(x0), x1))))
MARK.0(g.0(s.1(x0))) → ACTIVE.0(g.0(active.0(s.0(mark.1(x0)))))
MARK.0(g.0(cons.1-1(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(sel.0-1(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.0-0(g.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.0-0(y0, g.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(g.0(mark.1(x0)))))
MARK.0(sel.0-1(s.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.0(x0))), mark.1(y1)))
MARK.0(f.1(X)) → MARK.1(X)
MARK.0(sel.0-1(cons.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.1(x0), x1)), mark.1(y1)))
MARK.0(sel.0-1(X1, X2)) → MARK.0(X1)
ACTIVE.0(sel.0-0(s.0(X), cons.0-0(Y, Z))) → MARK.0(sel.0-0(X, Z))
MARK.0(sel.0-0(s.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.0(x0))), mark.0(y1)))
MARK.0(sel.0-0(y0, sel.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(g.0(sel.1-1(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.0-1(y0, x1)) → ACTIVE.0(sel.0-1(mark.0(y0), x1))
MARK.0(sel.0-1(f.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.1-0(y0, cons.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-0(mark.1(x0), x1))))
MARK.0(sel.0-1(g.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.0(x0))), mark.1(y1)))
ACTIVE.0(g.0(s.0(X))) → MARK.0(s.0(s.0(g.0(X))))
MARK.0(sel.0-0(y0, g.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(g.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.0(x0), x1)), mark.0(y1)))
MARK.0(sel.0-0(g.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.0(x0))), mark.0(y1)))
ACTIVE.0(g.0(s.1(X))) → MARK.0(s.0(s.0(g.1(X))))
MARK.0(g.1(X)) → MARK.1(X)
MARK.0(sel.1-0(y0, s.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(s.0(mark.0(x0)))))
MARK.0(sel.0-1(g.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.1(x0))), mark.1(y1)))
MARK.0(g.0(sel.0-0(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(sel.0-0(y0, cons.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(g.1(x0))) → ACTIVE.0(g.0(active.0(g.0(mark.1(x0)))))
MARK.0(sel.0-0(x0, y1)) → ACTIVE.0(sel.0-0(x0, mark.0(y1)))
MARK.0(sel.0-0(y0, x1)) → ACTIVE.0(sel.0-0(mark.0(y0), x1))
ACTIVE.0(sel.1-0(0., cons.0-0(X, Y))) → MARK.0(X)
MARK.0(sel.0-1(sel.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.1(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.1-0(Y, Z))) → MARK.0(sel.1-0(X, Z))
MARK.0(f.1(X)) → ACTIVE.0(f.0(mark.1(X)))
MARK.0(g.0(sel.1-0(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(sel.0-1(sel.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.0(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.1-1(Y, Z))) → MARK.0(sel.1-1(X, Z))
MARK.0(sel.1-0(y0, sel.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, x1)) → ACTIVE.0(sel.0-0(mark.1(y0), x1))
MARK.0(sel.0-0(y0, sel.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(sel.1-0(y0, cons.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-1(mark.0(x0), x1))))
MARK.0(sel.1-0(y0, sel.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(g.0(cons.1-0(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-0(mark.1(x0), x1))))
ACTIVE.0(sel.1-0(0., cons.1-1(X, Y))) → MARK.1(X)
ACTIVE.0(f.1(X)) → MARK.0(cons.1-0(X, f.0(g.1(X))))
ACTIVE.0(f.0(X)) → MARK.0(cons.0-0(X, f.0(g.0(X))))
MARK.0(sel.0-0(y0, s.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(s.0(mark.1(x0)))))
MARK.0(g.0(g.0(x0))) → ACTIVE.0(g.0(active.0(g.0(mark.0(x0)))))
MARK.0(sel.1-0(y0, g.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(g.0(mark.1(x0)))))
MARK.0(cons.0-0(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-1(cons.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.0(x0), x1)), mark.1(y1)))
MARK.0(sel.0-0(f.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.1-1(x0, y1)) → ACTIVE.0(sel.1-0(x0, mark.1(y1)))
MARK.0(sel.1-0(y0, sel.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(s.1(X)) → MARK.1(X)
MARK.0(sel.1-0(y0, sel.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, f.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(f.0(mark.1(x0)))))
MARK.0(sel.0-1(cons.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.0(x0), x1)), mark.1(y1)))
MARK.0(g.1(0.)) → ACTIVE.0(g.0(active.1(0.)))
MARK.0(sel.0-1(X1, X2)) → MARK.1(X2)
MARK.0(sel.0-1(sel.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.0(x1))), mark.1(y1)))
MARK.0(g.0(cons.0-0(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-0(mark.0(x0), x1))))
MARK.0(sel.0-0(cons.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.0(x0), x1)), mark.0(y1)))
MARK.0(sel.1-0(y0, g.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(g.0(mark.0(x0)))))
MARK.0(sel.0-0(s.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.1(x0))), mark.0(y1)))
MARK.0(cons.0-1(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-1(y0, 0.)) → ACTIVE.0(sel.0-0(mark.0(y0), active.1(0.)))
MARK.0(sel.0-0(y0, f.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(f.0(mark.0(x0)))))
MARK.0(g.0(X)) → MARK.0(X)
MARK.0(g.0(s.0(x0))) → ACTIVE.0(g.0(active.0(s.0(mark.0(x0)))))
MARK.0(sel.0-0(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-0(X1, X2)) → MARK.0(X2)
ACTIVE.0(sel.1-0(0., cons.1-0(X, Y))) → MARK.1(X)
ACTIVE.0(sel.0-0(s.0(X), cons.1-1(Y, Z))) → MARK.0(sel.0-1(X, Z))
MARK.0(sel.0-0(y0, s.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(s.0(mark.0(x0)))))
MARK.0(f.0(X)) → ACTIVE.0(f.0(mark.0(X)))
MARK.0(sel.0-0(sel.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.1(x1))), mark.0(y1)))
MARK.0(sel.1-0(y0, s.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(s.0(mark.1(x0)))))
MARK.0(cons.1-1(X1, X2)) → MARK.1(X1)
MARK.0(cons.1-0(X1, X2)) → MARK.1(X1)
ACTIVE.0(g.1(0.)) → MARK.0(s.1(0.))
MARK.0(sel.0-1(s.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.0-0(y0, sel.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(X1, X2)) → MARK.0(X2)
MARK.0(sel.0-1(sel.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.1(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.0(X), cons.1-0(Y, Z))) → MARK.0(sel.0-0(X, Z))
ACTIVE.0(sel.0-0(s.0(X), cons.0-1(Y, Z))) → MARK.0(sel.0-1(X, Z))
MARK.0(sel.0-0(y0, cons.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-0(mark.0(x0), x1))))
MARK.0(g.1(x0)) → ACTIVE.0(g.1(x0))
MARK.0(sel.1-1(y0, x1)) → ACTIVE.0(sel.0-1(mark.1(y0), x1))
MARK.0(sel.1-1(X1, X2)) → MARK.1(X2)
MARK.0(sel.1-0(0., y1)) → ACTIVE.0(sel.0-0(active.1(0.), mark.0(y1)))
MARK.0(s.0(X)) → MARK.0(X)
MARK.0(sel.1-0(y0, cons.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(cons.0-1(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-1(mark.0(x0), x1))))

The TRS R consists of the following rules:

sel.0-1(active.1(X1), X2) → sel.1-1(X1, X2)
mark.0(sel.1-1(X1, X2)) → active.0(sel.0-0(mark.1(X1), mark.1(X2)))
cons.1-0(X1, active.0(X2)) → cons.1-0(X1, X2)
mark.0(cons.1-1(X1, X2)) → active.0(cons.0-1(mark.1(X1), X2))
g.0(active.0(X)) → g.0(X)
cons.0-0(X1, active.1(X2)) → cons.0-1(X1, X2)
active.0(f.1(X)) → mark.0(cons.1-0(X, f.0(g.1(X))))
cons.0-1(active.0(X1), X2) → cons.0-1(X1, X2)
active.0(sel.0-0(s.0(X), cons.1-0(Y, Z))) → mark.0(sel.0-0(X, Z))
sel.1-0(X1, active.1(X2)) → sel.1-1(X1, X2)
cons.0-0(X1, mark.1(X2)) → cons.0-1(X1, X2)
sel.0-1(active.0(X1), X2) → sel.0-1(X1, X2)
cons.1-0(X1, active.1(X2)) → cons.1-1(X1, X2)
cons.0-0(active.0(X1), X2) → cons.0-0(X1, X2)
mark.0(cons.0-1(X1, X2)) → active.0(cons.0-1(mark.0(X1), X2))
mark.0(sel.0-0(X1, X2)) → active.0(sel.0-0(mark.0(X1), mark.0(X2)))
mark.0(s.0(X)) → active.0(s.0(mark.0(X)))
active.0(sel.0-0(s.1(X), cons.1-0(Y, Z))) → mark.0(sel.1-0(X, Z))
mark.0(f.1(X)) → active.0(f.0(mark.1(X)))
sel.0-0(mark.1(X1), X2) → sel.1-0(X1, X2)
sel.0-0(X1, mark.0(X2)) → sel.0-0(X1, X2)
cons.0-1(mark.0(X1), X2) → cons.0-1(X1, X2)
cons.0-0(X1, mark.0(X2)) → cons.0-0(X1, X2)
sel.0-0(X1, mark.1(X2)) → sel.0-1(X1, X2)
cons.0-0(active.1(X1), X2) → cons.1-0(X1, X2)
active.0(sel.0-0(s.1(X), cons.1-1(Y, Z))) → mark.0(sel.1-1(X, Z))
f.0(mark.0(X)) → f.0(X)
f.0(active.1(X)) → f.1(X)
g.0(mark.0(X)) → g.0(X)
cons.1-0(X1, mark.0(X2)) → cons.1-0(X1, X2)
active.0(g.0(s.1(X))) → mark.0(s.0(s.0(g.1(X))))
sel.0-1(mark.1(X1), X2) → sel.1-1(X1, X2)
active.0(sel.0-0(s.0(X), cons.0-1(Y, Z))) → mark.0(sel.0-1(X, Z))
cons.0-0(X1, active.0(X2)) → cons.0-0(X1, X2)
mark.0(s.1(X)) → active.0(s.0(mark.1(X)))
active.0(sel.1-0(0., cons.1-0(X, Y))) → mark.1(X)
mark.0(cons.0-0(X1, X2)) → active.0(cons.0-0(mark.0(X1), X2))
cons.1-0(X1, mark.1(X2)) → cons.1-1(X1, X2)
sel.0-1(mark.0(X1), X2) → sel.0-1(X1, X2)
mark.1(0.) → active.1(0.)
active.0(sel.0-0(s.1(X), cons.0-1(Y, Z))) → mark.0(sel.1-1(X, Z))
sel.1-0(X1, active.0(X2)) → sel.1-0(X1, X2)
active.0(g.0(s.0(X))) → mark.0(s.0(s.0(g.0(X))))
sel.0-0(active.0(X1), X2) → sel.0-0(X1, X2)
cons.0-1(mark.1(X1), X2) → cons.1-1(X1, X2)
sel.0-0(X1, active.0(X2)) → sel.0-0(X1, X2)
s.0(active.0(X)) → s.0(X)
sel.0-0(active.1(X1), X2) → sel.1-0(X1, X2)
cons.0-1(active.1(X1), X2) → cons.1-1(X1, X2)
mark.0(g.1(X)) → active.0(g.0(mark.1(X)))
f.0(active.0(X)) → f.0(X)
s.0(mark.1(X)) → s.1(X)
sel.0-0(mark.0(X1), X2) → sel.0-0(X1, X2)
active.0(sel.0-0(s.1(X), cons.0-0(Y, Z))) → mark.0(sel.1-0(X, Z))
active.0(sel.0-0(s.0(X), cons.0-0(Y, Z))) → mark.0(sel.0-0(X, Z))
sel.1-0(X1, mark.0(X2)) → sel.1-0(X1, X2)
active.0(sel.1-0(0., cons.0-0(X, Y))) → mark.0(X)
active.0(g.1(0.)) → mark.0(s.1(0.))
sel.0-0(X1, active.1(X2)) → sel.0-1(X1, X2)
g.0(active.1(X)) → g.1(X)
mark.0(sel.1-0(X1, X2)) → active.0(sel.0-0(mark.1(X1), mark.0(X2)))
s.0(active.1(X)) → s.1(X)
mark.0(f.0(X)) → active.0(f.0(mark.0(X)))
active.0(sel.0-0(s.0(X), cons.1-1(Y, Z))) → mark.0(sel.0-1(X, Z))
cons.0-0(mark.1(X1), X2) → cons.1-0(X1, X2)
sel.1-0(X1, mark.1(X2)) → sel.1-1(X1, X2)
mark.0(cons.1-0(X1, X2)) → active.0(cons.0-0(mark.1(X1), X2))
active.0(sel.1-0(0., cons.0-1(X, Y))) → mark.0(X)
mark.0(g.0(X)) → active.0(g.0(mark.0(X)))
g.0(mark.1(X)) → g.1(X)
s.0(mark.0(X)) → s.0(X)
f.0(mark.1(X)) → f.1(X)
active.0(f.0(X)) → mark.0(cons.0-0(X, f.0(g.0(X))))
active.0(sel.1-0(0., cons.1-1(X, Y))) → mark.1(X)
cons.0-0(mark.0(X1), X2) → cons.0-0(X1, X2)
mark.0(sel.0-1(X1, X2)) → active.0(sel.0-0(mark.0(X1), mark.1(X2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 14 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ SemLabProof
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ QDPOrderProof
                        ↳ SemLabProof2

Q DP problem:
The TRS P consists of the following rules:

MARK.0(g.0(f.0(x0))) → ACTIVE.0(g.0(active.0(f.0(mark.0(x0)))))
MARK.0(f.0(X)) → MARK.0(X)
ACTIVE.0(sel.0-0(s.1(X), cons.0-1(Y, Z))) → MARK.0(sel.1-1(X, Z))
MARK.0(sel.1-0(x0, y1)) → ACTIVE.0(sel.1-0(x0, mark.0(y1)))
MARK.0(sel.0-0(y0, cons.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-1(mark.0(x0), x1))))
MARK.0(sel.0-1(cons.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.1(x0), x1)), mark.1(y1)))
MARK.0(sel.1-0(y0, f.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(f.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.1(x0), x1)), mark.0(y1)))
MARK.0(sel.1-0(y0, cons.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-0(mark.0(x0), x1))))
ACTIVE.0(sel.0-0(s.1(X), cons.0-0(Y, Z))) → MARK.0(sel.1-0(X, Z))
MARK.0(g.0(x0)) → ACTIVE.0(g.0(x0))
MARK.0(sel.0-0(cons.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.1(x0), x1)), mark.0(y1)))
ACTIVE.0(sel.1-0(0., cons.0-1(X, Y))) → MARK.0(X)
MARK.0(sel.0-1(f.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.0(x0))), mark.1(y1)))
MARK.0(sel.0-1(x0, y1)) → ACTIVE.0(sel.0-0(x0, mark.1(y1)))
MARK.0(sel.0-0(sel.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.0(x1))), mark.0(y1)))
MARK.0(sel.0-0(y0, sel.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.0-0(f.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.0(x0))), mark.0(y1)))
MARK.0(sel.0-0(sel.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.0(x1))), mark.0(y1)))
MARK.0(sel.0-0(sel.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.1(x1))), mark.0(y1)))
MARK.0(g.0(f.1(x0))) → ACTIVE.0(g.0(active.0(f.0(mark.1(x0)))))
MARK.0(sel.1-1(y0, 0.)) → ACTIVE.0(sel.0-0(mark.1(y0), active.1(0.)))
MARK.0(sel.1-1(0., y1)) → ACTIVE.0(sel.0-0(active.1(0.), mark.1(y1)))
MARK.0(sel.0-0(y0, f.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(f.0(mark.1(x0)))))
MARK.0(sel.0-0(y0, cons.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-0(mark.1(x0), x1))))
MARK.0(g.0(s.1(x0))) → ACTIVE.0(g.0(active.0(s.0(mark.1(x0)))))
MARK.0(g.0(cons.1-1(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(sel.0-1(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.0-0(g.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.0-0(y0, g.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(g.0(mark.1(x0)))))
MARK.0(sel.0-1(s.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.0(x0))), mark.1(y1)))
MARK.0(sel.0-1(cons.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.1(x0), x1)), mark.1(y1)))
MARK.0(sel.0-1(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-0(s.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.0(x0))), mark.0(y1)))
ACTIVE.0(sel.0-0(s.0(X), cons.0-0(Y, Z))) → MARK.0(sel.0-0(X, Z))
MARK.0(sel.0-0(y0, sel.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(g.0(sel.1-1(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.0-1(y0, x1)) → ACTIVE.0(sel.0-1(mark.0(y0), x1))
MARK.0(sel.0-1(f.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.1-0(y0, cons.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-0(mark.1(x0), x1))))
MARK.0(sel.0-1(g.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.0(x0))), mark.1(y1)))
ACTIVE.0(g.0(s.0(X))) → MARK.0(s.0(s.0(g.0(X))))
MARK.0(sel.0-0(y0, g.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(g.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.0(x0), x1)), mark.0(y1)))
MARK.0(sel.0-0(g.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.0(x0))), mark.0(y1)))
ACTIVE.0(g.0(s.1(X))) → MARK.0(s.0(s.0(g.1(X))))
MARK.0(sel.1-0(y0, s.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(s.0(mark.0(x0)))))
MARK.0(sel.0-1(g.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.1(x0))), mark.1(y1)))
MARK.0(g.0(sel.0-0(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(sel.0-0(y0, cons.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(g.1(x0))) → ACTIVE.0(g.0(active.0(g.0(mark.1(x0)))))
MARK.0(sel.0-0(x0, y1)) → ACTIVE.0(sel.0-0(x0, mark.0(y1)))
MARK.0(sel.0-0(y0, x1)) → ACTIVE.0(sel.0-0(mark.0(y0), x1))
ACTIVE.0(sel.1-0(0., cons.0-0(X, Y))) → MARK.0(X)
MARK.0(sel.0-1(sel.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.1(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.1-0(Y, Z))) → MARK.0(sel.1-0(X, Z))
MARK.0(f.1(X)) → ACTIVE.0(f.0(mark.1(X)))
MARK.0(g.0(sel.1-0(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(sel.0-1(sel.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.0(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.1-1(Y, Z))) → MARK.0(sel.1-1(X, Z))
MARK.0(sel.1-0(y0, sel.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, x1)) → ACTIVE.0(sel.0-0(mark.1(y0), x1))
MARK.0(sel.0-0(y0, sel.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(sel.1-0(y0, cons.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-1(mark.0(x0), x1))))
MARK.0(sel.1-0(y0, sel.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(g.0(cons.1-0(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-0(mark.1(x0), x1))))
ACTIVE.0(f.0(X)) → MARK.0(cons.0-0(X, f.0(g.0(X))))
MARK.0(sel.0-0(y0, s.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(s.0(mark.1(x0)))))
MARK.0(sel.1-0(y0, g.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(g.0(mark.1(x0)))))
MARK.0(g.0(g.0(x0))) → ACTIVE.0(g.0(active.0(g.0(mark.0(x0)))))
MARK.0(cons.0-0(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-1(cons.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.0(x0), x1)), mark.1(y1)))
MARK.0(sel.0-0(f.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.1-1(x0, y1)) → ACTIVE.0(sel.1-0(x0, mark.1(y1)))
MARK.0(sel.1-0(y0, sel.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(sel.1-0(y0, sel.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, f.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(f.0(mark.1(x0)))))
MARK.0(sel.0-1(cons.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.0(x0), x1)), mark.1(y1)))
MARK.0(g.1(0.)) → ACTIVE.0(g.0(active.1(0.)))
MARK.0(g.0(cons.0-0(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-0(mark.0(x0), x1))))
MARK.0(sel.0-1(sel.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.0(x1))), mark.1(y1)))
MARK.0(sel.1-0(y0, g.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(g.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.0(x0), x1)), mark.0(y1)))
MARK.0(sel.0-0(s.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.0-1(y0, 0.)) → ACTIVE.0(sel.0-0(mark.0(y0), active.1(0.)))
MARK.0(cons.0-1(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-0(y0, f.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(f.0(mark.0(x0)))))
MARK.0(g.0(X)) → MARK.0(X)
MARK.0(g.0(s.0(x0))) → ACTIVE.0(g.0(active.0(s.0(mark.0(x0)))))
MARK.0(sel.0-0(X1, X2)) → MARK.0(X2)
MARK.0(sel.0-0(X1, X2)) → MARK.0(X1)
ACTIVE.0(sel.0-0(s.0(X), cons.1-1(Y, Z))) → MARK.0(sel.0-1(X, Z))
MARK.0(sel.0-0(y0, s.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(s.0(mark.0(x0)))))
MARK.0(f.0(X)) → ACTIVE.0(f.0(mark.0(X)))
MARK.0(sel.0-0(sel.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.1(x1))), mark.0(y1)))
MARK.0(sel.1-0(y0, s.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(s.0(mark.1(x0)))))
MARK.0(sel.0-1(s.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.0-0(y0, sel.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(X1, X2)) → MARK.0(X2)
MARK.0(sel.0-1(sel.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.1(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.0(X), cons.0-1(Y, Z))) → MARK.0(sel.0-1(X, Z))
ACTIVE.0(sel.0-0(s.0(X), cons.1-0(Y, Z))) → MARK.0(sel.0-0(X, Z))
MARK.0(sel.0-0(y0, cons.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-0(mark.0(x0), x1))))
MARK.0(sel.1-1(y0, x1)) → ACTIVE.0(sel.0-1(mark.1(y0), x1))
MARK.0(sel.1-0(0., y1)) → ACTIVE.0(sel.0-0(active.1(0.), mark.0(y1)))
MARK.0(s.0(X)) → MARK.0(X)
MARK.0(sel.1-0(y0, cons.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(cons.0-1(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-1(mark.0(x0), x1))))

The TRS R consists of the following rules:

sel.0-1(active.1(X1), X2) → sel.1-1(X1, X2)
mark.0(sel.1-1(X1, X2)) → active.0(sel.0-0(mark.1(X1), mark.1(X2)))
cons.1-0(X1, active.0(X2)) → cons.1-0(X1, X2)
mark.0(cons.1-1(X1, X2)) → active.0(cons.0-1(mark.1(X1), X2))
g.0(active.0(X)) → g.0(X)
cons.0-0(X1, active.1(X2)) → cons.0-1(X1, X2)
active.0(f.1(X)) → mark.0(cons.1-0(X, f.0(g.1(X))))
cons.0-1(active.0(X1), X2) → cons.0-1(X1, X2)
active.0(sel.0-0(s.0(X), cons.1-0(Y, Z))) → mark.0(sel.0-0(X, Z))
sel.1-0(X1, active.1(X2)) → sel.1-1(X1, X2)
cons.0-0(X1, mark.1(X2)) → cons.0-1(X1, X2)
sel.0-1(active.0(X1), X2) → sel.0-1(X1, X2)
cons.1-0(X1, active.1(X2)) → cons.1-1(X1, X2)
cons.0-0(active.0(X1), X2) → cons.0-0(X1, X2)
mark.0(cons.0-1(X1, X2)) → active.0(cons.0-1(mark.0(X1), X2))
mark.0(sel.0-0(X1, X2)) → active.0(sel.0-0(mark.0(X1), mark.0(X2)))
mark.0(s.0(X)) → active.0(s.0(mark.0(X)))
active.0(sel.0-0(s.1(X), cons.1-0(Y, Z))) → mark.0(sel.1-0(X, Z))
mark.0(f.1(X)) → active.0(f.0(mark.1(X)))
sel.0-0(mark.1(X1), X2) → sel.1-0(X1, X2)
sel.0-0(X1, mark.0(X2)) → sel.0-0(X1, X2)
cons.0-1(mark.0(X1), X2) → cons.0-1(X1, X2)
cons.0-0(X1, mark.0(X2)) → cons.0-0(X1, X2)
sel.0-0(X1, mark.1(X2)) → sel.0-1(X1, X2)
cons.0-0(active.1(X1), X2) → cons.1-0(X1, X2)
active.0(sel.0-0(s.1(X), cons.1-1(Y, Z))) → mark.0(sel.1-1(X, Z))
f.0(mark.0(X)) → f.0(X)
f.0(active.1(X)) → f.1(X)
g.0(mark.0(X)) → g.0(X)
cons.1-0(X1, mark.0(X2)) → cons.1-0(X1, X2)
active.0(g.0(s.1(X))) → mark.0(s.0(s.0(g.1(X))))
sel.0-1(mark.1(X1), X2) → sel.1-1(X1, X2)
active.0(sel.0-0(s.0(X), cons.0-1(Y, Z))) → mark.0(sel.0-1(X, Z))
cons.0-0(X1, active.0(X2)) → cons.0-0(X1, X2)
mark.0(s.1(X)) → active.0(s.0(mark.1(X)))
active.0(sel.1-0(0., cons.1-0(X, Y))) → mark.1(X)
mark.0(cons.0-0(X1, X2)) → active.0(cons.0-0(mark.0(X1), X2))
cons.1-0(X1, mark.1(X2)) → cons.1-1(X1, X2)
sel.0-1(mark.0(X1), X2) → sel.0-1(X1, X2)
mark.1(0.) → active.1(0.)
active.0(sel.0-0(s.1(X), cons.0-1(Y, Z))) → mark.0(sel.1-1(X, Z))
sel.1-0(X1, active.0(X2)) → sel.1-0(X1, X2)
active.0(g.0(s.0(X))) → mark.0(s.0(s.0(g.0(X))))
sel.0-0(active.0(X1), X2) → sel.0-0(X1, X2)
cons.0-1(mark.1(X1), X2) → cons.1-1(X1, X2)
sel.0-0(X1, active.0(X2)) → sel.0-0(X1, X2)
s.0(active.0(X)) → s.0(X)
sel.0-0(active.1(X1), X2) → sel.1-0(X1, X2)
cons.0-1(active.1(X1), X2) → cons.1-1(X1, X2)
mark.0(g.1(X)) → active.0(g.0(mark.1(X)))
f.0(active.0(X)) → f.0(X)
s.0(mark.1(X)) → s.1(X)
sel.0-0(mark.0(X1), X2) → sel.0-0(X1, X2)
active.0(sel.0-0(s.1(X), cons.0-0(Y, Z))) → mark.0(sel.1-0(X, Z))
active.0(sel.0-0(s.0(X), cons.0-0(Y, Z))) → mark.0(sel.0-0(X, Z))
sel.1-0(X1, mark.0(X2)) → sel.1-0(X1, X2)
active.0(sel.1-0(0., cons.0-0(X, Y))) → mark.0(X)
active.0(g.1(0.)) → mark.0(s.1(0.))
sel.0-0(X1, active.1(X2)) → sel.0-1(X1, X2)
g.0(active.1(X)) → g.1(X)
mark.0(sel.1-0(X1, X2)) → active.0(sel.0-0(mark.1(X1), mark.0(X2)))
s.0(active.1(X)) → s.1(X)
mark.0(f.0(X)) → active.0(f.0(mark.0(X)))
active.0(sel.0-0(s.0(X), cons.1-1(Y, Z))) → mark.0(sel.0-1(X, Z))
cons.0-0(mark.1(X1), X2) → cons.1-0(X1, X2)
sel.1-0(X1, mark.1(X2)) → sel.1-1(X1, X2)
mark.0(cons.1-0(X1, X2)) → active.0(cons.0-0(mark.1(X1), X2))
active.0(sel.1-0(0., cons.0-1(X, Y))) → mark.0(X)
mark.0(g.0(X)) → active.0(g.0(mark.0(X)))
g.0(mark.1(X)) → g.1(X)
s.0(mark.0(X)) → s.0(X)
f.0(mark.1(X)) → f.1(X)
active.0(f.0(X)) → mark.0(cons.0-0(X, f.0(g.0(X))))
active.0(sel.1-0(0., cons.1-1(X, Y))) → mark.1(X)
cons.0-0(mark.0(X1), X2) → cons.0-0(X1, X2)
mark.0(sel.0-1(X1, X2)) → active.0(sel.0-0(mark.0(X1), mark.1(X2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


MARK.0(sel.0-1(y0, x1)) → ACTIVE.0(sel.0-1(mark.0(y0), x1))
MARK.0(sel.1-1(y0, x1)) → ACTIVE.0(sel.0-1(mark.1(y0), x1))
The remaining pairs can at least be oriented weakly.

MARK.0(g.0(f.0(x0))) → ACTIVE.0(g.0(active.0(f.0(mark.0(x0)))))
MARK.0(f.0(X)) → MARK.0(X)
ACTIVE.0(sel.0-0(s.1(X), cons.0-1(Y, Z))) → MARK.0(sel.1-1(X, Z))
MARK.0(sel.1-0(x0, y1)) → ACTIVE.0(sel.1-0(x0, mark.0(y1)))
MARK.0(sel.0-0(y0, cons.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-1(mark.0(x0), x1))))
MARK.0(sel.0-1(cons.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.1(x0), x1)), mark.1(y1)))
MARK.0(sel.1-0(y0, f.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(f.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.1(x0), x1)), mark.0(y1)))
MARK.0(sel.1-0(y0, cons.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-0(mark.0(x0), x1))))
ACTIVE.0(sel.0-0(s.1(X), cons.0-0(Y, Z))) → MARK.0(sel.1-0(X, Z))
MARK.0(g.0(x0)) → ACTIVE.0(g.0(x0))
MARK.0(sel.0-0(cons.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.1(x0), x1)), mark.0(y1)))
ACTIVE.0(sel.1-0(0., cons.0-1(X, Y))) → MARK.0(X)
MARK.0(sel.0-1(f.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.0(x0))), mark.1(y1)))
MARK.0(sel.0-1(x0, y1)) → ACTIVE.0(sel.0-0(x0, mark.1(y1)))
MARK.0(sel.0-0(sel.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.0(x1))), mark.0(y1)))
MARK.0(sel.0-0(y0, sel.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.0-0(f.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.0(x0))), mark.0(y1)))
MARK.0(sel.0-0(sel.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.0(x1))), mark.0(y1)))
MARK.0(sel.0-0(sel.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.1(x1))), mark.0(y1)))
MARK.0(g.0(f.1(x0))) → ACTIVE.0(g.0(active.0(f.0(mark.1(x0)))))
MARK.0(sel.1-1(y0, 0.)) → ACTIVE.0(sel.0-0(mark.1(y0), active.1(0.)))
MARK.0(sel.1-1(0., y1)) → ACTIVE.0(sel.0-0(active.1(0.), mark.1(y1)))
MARK.0(sel.0-0(y0, f.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(f.0(mark.1(x0)))))
MARK.0(sel.0-0(y0, cons.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-0(mark.1(x0), x1))))
MARK.0(g.0(s.1(x0))) → ACTIVE.0(g.0(active.0(s.0(mark.1(x0)))))
MARK.0(g.0(cons.1-1(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(sel.0-1(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.0-0(g.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.0-0(y0, g.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(g.0(mark.1(x0)))))
MARK.0(sel.0-1(s.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.0(x0))), mark.1(y1)))
MARK.0(sel.0-1(cons.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.1(x0), x1)), mark.1(y1)))
MARK.0(sel.0-1(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-0(s.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.0(x0))), mark.0(y1)))
ACTIVE.0(sel.0-0(s.0(X), cons.0-0(Y, Z))) → MARK.0(sel.0-0(X, Z))
MARK.0(sel.0-0(y0, sel.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(g.0(sel.1-1(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.0-1(f.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.1-0(y0, cons.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-0(mark.1(x0), x1))))
MARK.0(sel.0-1(g.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.0(x0))), mark.1(y1)))
ACTIVE.0(g.0(s.0(X))) → MARK.0(s.0(s.0(g.0(X))))
MARK.0(sel.0-0(y0, g.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(g.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.0(x0), x1)), mark.0(y1)))
MARK.0(sel.0-0(g.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.0(x0))), mark.0(y1)))
ACTIVE.0(g.0(s.1(X))) → MARK.0(s.0(s.0(g.1(X))))
MARK.0(sel.1-0(y0, s.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(s.0(mark.0(x0)))))
MARK.0(sel.0-1(g.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.1(x0))), mark.1(y1)))
MARK.0(g.0(sel.0-0(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(sel.0-0(y0, cons.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(g.1(x0))) → ACTIVE.0(g.0(active.0(g.0(mark.1(x0)))))
MARK.0(sel.0-0(x0, y1)) → ACTIVE.0(sel.0-0(x0, mark.0(y1)))
MARK.0(sel.0-0(y0, x1)) → ACTIVE.0(sel.0-0(mark.0(y0), x1))
ACTIVE.0(sel.1-0(0., cons.0-0(X, Y))) → MARK.0(X)
MARK.0(sel.0-1(sel.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.1(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.1-0(Y, Z))) → MARK.0(sel.1-0(X, Z))
MARK.0(f.1(X)) → ACTIVE.0(f.0(mark.1(X)))
MARK.0(g.0(sel.1-0(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(sel.0-1(sel.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.0(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.1-1(Y, Z))) → MARK.0(sel.1-1(X, Z))
MARK.0(sel.1-0(y0, sel.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, x1)) → ACTIVE.0(sel.0-0(mark.1(y0), x1))
MARK.0(sel.0-0(y0, sel.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(sel.1-0(y0, cons.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-1(mark.0(x0), x1))))
MARK.0(sel.1-0(y0, sel.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(g.0(cons.1-0(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-0(mark.1(x0), x1))))
ACTIVE.0(f.0(X)) → MARK.0(cons.0-0(X, f.0(g.0(X))))
MARK.0(sel.0-0(y0, s.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(s.0(mark.1(x0)))))
MARK.0(sel.1-0(y0, g.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(g.0(mark.1(x0)))))
MARK.0(g.0(g.0(x0))) → ACTIVE.0(g.0(active.0(g.0(mark.0(x0)))))
MARK.0(cons.0-0(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-1(cons.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.0(x0), x1)), mark.1(y1)))
MARK.0(sel.0-0(f.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.1-1(x0, y1)) → ACTIVE.0(sel.1-0(x0, mark.1(y1)))
MARK.0(sel.1-0(y0, sel.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(sel.1-0(y0, sel.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, f.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(f.0(mark.1(x0)))))
MARK.0(sel.0-1(cons.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.0(x0), x1)), mark.1(y1)))
MARK.0(g.1(0.)) → ACTIVE.0(g.0(active.1(0.)))
MARK.0(g.0(cons.0-0(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-0(mark.0(x0), x1))))
MARK.0(sel.0-1(sel.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.0(x1))), mark.1(y1)))
MARK.0(sel.1-0(y0, g.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(g.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.0(x0), x1)), mark.0(y1)))
MARK.0(sel.0-0(s.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.0-1(y0, 0.)) → ACTIVE.0(sel.0-0(mark.0(y0), active.1(0.)))
MARK.0(cons.0-1(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-0(y0, f.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(f.0(mark.0(x0)))))
MARK.0(g.0(X)) → MARK.0(X)
MARK.0(g.0(s.0(x0))) → ACTIVE.0(g.0(active.0(s.0(mark.0(x0)))))
MARK.0(sel.0-0(X1, X2)) → MARK.0(X2)
MARK.0(sel.0-0(X1, X2)) → MARK.0(X1)
ACTIVE.0(sel.0-0(s.0(X), cons.1-1(Y, Z))) → MARK.0(sel.0-1(X, Z))
MARK.0(sel.0-0(y0, s.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(s.0(mark.0(x0)))))
MARK.0(f.0(X)) → ACTIVE.0(f.0(mark.0(X)))
MARK.0(sel.0-0(sel.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.1(x1))), mark.0(y1)))
MARK.0(sel.1-0(y0, s.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(s.0(mark.1(x0)))))
MARK.0(sel.0-1(s.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.0-0(y0, sel.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(X1, X2)) → MARK.0(X2)
MARK.0(sel.0-1(sel.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.1(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.0(X), cons.0-1(Y, Z))) → MARK.0(sel.0-1(X, Z))
ACTIVE.0(sel.0-0(s.0(X), cons.1-0(Y, Z))) → MARK.0(sel.0-0(X, Z))
MARK.0(sel.0-0(y0, cons.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-0(mark.0(x0), x1))))
MARK.0(sel.1-0(0., y1)) → ACTIVE.0(sel.0-0(active.1(0.), mark.0(y1)))
MARK.0(s.0(X)) → MARK.0(X)
MARK.0(sel.1-0(y0, cons.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(cons.0-1(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-1(mark.0(x0), x1))))
Used ordering: Polynomial interpretation [25]:

POL(0.) = 0   
POL(ACTIVE.0(x1)) = x1   
POL(MARK.0(x1)) = 1   
POL(active.0(x1)) = 0   
POL(active.1(x1)) = 0   
POL(cons.0-0(x1, x2)) = 0   
POL(cons.0-1(x1, x2)) = 0   
POL(cons.1-0(x1, x2)) = 0   
POL(cons.1-1(x1, x2)) = 0   
POL(f.0(x1)) = 1   
POL(f.1(x1)) = 1   
POL(g.0(x1)) = 1   
POL(g.1(x1)) = 0   
POL(mark.0(x1)) = 0   
POL(mark.1(x1)) = 0   
POL(s.0(x1)) = 0   
POL(s.1(x1)) = 0   
POL(sel.0-0(x1, x2)) = 1   
POL(sel.0-1(x1, x2)) = 0   
POL(sel.1-0(x1, x2)) = 1   
POL(sel.1-1(x1, x2)) = 0   

The following usable rules [17] were oriented:

sel.0-1(mark.1(X1), X2) → sel.1-1(X1, X2)
g.0(mark.0(X)) → g.0(X)
g.0(active.0(X)) → g.0(X)
f.0(active.1(X)) → f.1(X)
sel.0-0(X1, mark.1(X2)) → sel.0-1(X1, X2)
sel.0-0(mark.1(X1), X2) → sel.1-0(X1, X2)
sel.1-0(X1, active.1(X2)) → sel.1-1(X1, X2)
g.0(mark.1(X)) → g.1(X)
sel.1-0(X1, mark.1(X2)) → sel.1-1(X1, X2)
g.0(active.1(X)) → g.1(X)
sel.0-0(X1, active.1(X2)) → sel.0-1(X1, X2)
sel.1-0(X1, mark.0(X2)) → sel.1-0(X1, X2)
sel.1-0(X1, active.0(X2)) → sel.1-0(X1, X2)
f.0(active.0(X)) → f.0(X)
f.0(mark.0(X)) → f.0(X)
sel.0-0(active.1(X1), X2) → sel.1-0(X1, X2)
sel.0-0(active.0(X1), X2) → sel.0-0(X1, X2)
sel.0-0(X1, active.0(X2)) → sel.0-0(X1, X2)
sel.0-0(mark.0(X1), X2) → sel.0-0(X1, X2)
sel.0-0(X1, mark.0(X2)) → sel.0-0(X1, X2)
sel.0-1(mark.0(X1), X2) → sel.0-1(X1, X2)
sel.0-1(active.0(X1), X2) → sel.0-1(X1, X2)
f.0(mark.1(X)) → f.1(X)
sel.0-1(active.1(X1), X2) → sel.1-1(X1, X2)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ SemLabProof
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ QDPOrderProof
                                  ↳ QDP
                        ↳ SemLabProof2

Q DP problem:
The TRS P consists of the following rules:

MARK.0(g.0(f.0(x0))) → ACTIVE.0(g.0(active.0(f.0(mark.0(x0)))))
MARK.0(f.0(X)) → MARK.0(X)
MARK.0(sel.1-0(x0, y1)) → ACTIVE.0(sel.1-0(x0, mark.0(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.0-1(Y, Z))) → MARK.0(sel.1-1(X, Z))
MARK.0(sel.0-0(y0, cons.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-1(mark.0(x0), x1))))
MARK.0(sel.0-1(cons.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.1(x0), x1)), mark.1(y1)))
MARK.0(sel.1-0(y0, f.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(f.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.1(x0), x1)), mark.0(y1)))
MARK.0(sel.1-0(y0, cons.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-0(mark.0(x0), x1))))
ACTIVE.0(sel.0-0(s.1(X), cons.0-0(Y, Z))) → MARK.0(sel.1-0(X, Z))
MARK.0(g.0(x0)) → ACTIVE.0(g.0(x0))
MARK.0(sel.0-0(cons.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.1(x0), x1)), mark.0(y1)))
ACTIVE.0(sel.1-0(0., cons.0-1(X, Y))) → MARK.0(X)
MARK.0(sel.0-1(f.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.0(x0))), mark.1(y1)))
MARK.0(sel.0-1(x0, y1)) → ACTIVE.0(sel.0-0(x0, mark.1(y1)))
MARK.0(sel.0-0(sel.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.0(x1))), mark.0(y1)))
MARK.0(sel.0-0(y0, sel.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.0-0(f.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.0(x0))), mark.0(y1)))
MARK.0(sel.0-0(sel.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.0(x1))), mark.0(y1)))
MARK.0(sel.0-0(sel.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.1(x1))), mark.0(y1)))
MARK.0(g.0(f.1(x0))) → ACTIVE.0(g.0(active.0(f.0(mark.1(x0)))))
MARK.0(sel.1-1(y0, 0.)) → ACTIVE.0(sel.0-0(mark.1(y0), active.1(0.)))
MARK.0(sel.1-1(0., y1)) → ACTIVE.0(sel.0-0(active.1(0.), mark.1(y1)))
MARK.0(sel.0-0(y0, f.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(f.0(mark.1(x0)))))
MARK.0(sel.0-0(y0, cons.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-0(mark.1(x0), x1))))
MARK.0(g.0(s.1(x0))) → ACTIVE.0(g.0(active.0(s.0(mark.1(x0)))))
MARK.0(g.0(cons.1-1(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(sel.0-1(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.0-0(g.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.0-0(y0, g.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(g.0(mark.1(x0)))))
MARK.0(sel.0-1(s.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.0(x0))), mark.1(y1)))
MARK.0(sel.0-1(cons.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.1(x0), x1)), mark.1(y1)))
MARK.0(sel.0-1(X1, X2)) → MARK.0(X1)
ACTIVE.0(sel.0-0(s.0(X), cons.0-0(Y, Z))) → MARK.0(sel.0-0(X, Z))
MARK.0(sel.0-0(s.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.0(x0))), mark.0(y1)))
MARK.0(sel.0-0(y0, sel.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(g.0(sel.1-1(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, cons.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-0(mark.1(x0), x1))))
MARK.0(sel.0-1(f.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.0-1(g.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.0(x0))), mark.1(y1)))
ACTIVE.0(g.0(s.0(X))) → MARK.0(s.0(s.0(g.0(X))))
MARK.0(sel.0-0(y0, g.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(g.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.0(x0), x1)), mark.0(y1)))
MARK.0(sel.0-0(g.0(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.0(x0))), mark.0(y1)))
ACTIVE.0(g.0(s.1(X))) → MARK.0(s.0(s.0(g.1(X))))
MARK.0(sel.1-0(y0, s.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(s.0(mark.0(x0)))))
MARK.0(sel.0-1(g.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(g.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.0-0(y0, cons.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(sel.0-0(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(g.0(g.1(x0))) → ACTIVE.0(g.0(active.0(g.0(mark.1(x0)))))
MARK.0(sel.0-0(x0, y1)) → ACTIVE.0(sel.0-0(x0, mark.0(y1)))
MARK.0(sel.0-0(y0, x1)) → ACTIVE.0(sel.0-0(mark.0(y0), x1))
ACTIVE.0(sel.1-0(0., cons.0-0(X, Y))) → MARK.0(X)
MARK.0(sel.0-1(sel.1-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.1(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.1-0(Y, Z))) → MARK.0(sel.1-0(X, Z))
MARK.0(f.1(X)) → ACTIVE.0(f.0(mark.1(X)))
MARK.0(g.0(sel.1-0(x0, x1))) → ACTIVE.0(g.0(active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(sel.0-1(sel.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.0(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.1(X), cons.1-1(Y, Z))) → MARK.0(sel.1-1(X, Z))
MARK.0(sel.1-0(y0, sel.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.0(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, x1)) → ACTIVE.0(sel.0-0(mark.1(y0), x1))
MARK.0(sel.0-0(y0, sel.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(sel.1-0(y0, cons.0-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-1(mark.0(x0), x1))))
MARK.0(sel.1-0(y0, sel.1-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.1(x0), mark.0(x1)))))
MARK.0(g.0(cons.1-0(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-0(mark.1(x0), x1))))
ACTIVE.0(f.0(X)) → MARK.0(cons.0-0(X, f.0(g.0(X))))
MARK.0(sel.0-0(y0, s.1(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(s.0(mark.1(x0)))))
MARK.0(sel.1-0(y0, g.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(g.0(mark.1(x0)))))
MARK.0(g.0(g.0(x0))) → ACTIVE.0(g.0(active.0(g.0(mark.0(x0)))))
MARK.0(cons.0-0(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-1(cons.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.0(x0), x1)), mark.1(y1)))
MARK.0(sel.0-0(f.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(f.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.1-1(x0, y1)) → ACTIVE.0(sel.1-0(x0, mark.1(y1)))
MARK.0(sel.1-0(y0, sel.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.0(x0), mark.0(x1)))))
MARK.0(sel.1-0(y0, sel.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(y0, f.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(f.0(mark.1(x0)))))
MARK.0(sel.0-1(cons.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-1(mark.0(x0), x1)), mark.1(y1)))
MARK.0(g.1(0.)) → ACTIVE.0(g.0(active.1(0.)))
MARK.0(g.0(cons.0-0(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-0(mark.0(x0), x1))))
MARK.0(sel.0-1(sel.1-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.1(x0), mark.0(x1))), mark.1(y1)))
MARK.0(sel.1-0(y0, g.0(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(g.0(mark.0(x0)))))
MARK.0(sel.0-0(cons.0-0(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(cons.0-0(mark.0(x0), x1)), mark.0(y1)))
MARK.0(sel.0-0(s.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.1(x0))), mark.0(y1)))
MARK.0(sel.0-1(y0, 0.)) → ACTIVE.0(sel.0-0(mark.0(y0), active.1(0.)))
MARK.0(cons.0-1(X1, X2)) → MARK.0(X1)
MARK.0(sel.0-0(y0, f.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(f.0(mark.0(x0)))))
MARK.0(g.0(X)) → MARK.0(X)
MARK.0(g.0(s.0(x0))) → ACTIVE.0(g.0(active.0(s.0(mark.0(x0)))))
MARK.0(sel.0-0(X1, X2)) → MARK.0(X2)
MARK.0(sel.0-0(X1, X2)) → MARK.0(X1)
ACTIVE.0(sel.0-0(s.0(X), cons.1-1(Y, Z))) → MARK.0(sel.0-1(X, Z))
MARK.0(sel.0-0(y0, s.0(x0))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(s.0(mark.0(x0)))))
MARK.0(f.0(X)) → ACTIVE.0(f.0(mark.0(X)))
MARK.0(sel.0-0(sel.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.1(x1))), mark.0(y1)))
MARK.0(sel.1-0(y0, s.1(x0))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(s.0(mark.1(x0)))))
MARK.0(sel.0-1(s.1(x0), y1)) → ACTIVE.0(sel.0-0(active.0(s.0(mark.1(x0))), mark.1(y1)))
MARK.0(sel.0-0(y0, sel.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(sel.0-0(mark.1(x0), mark.1(x1)))))
MARK.0(sel.1-0(X1, X2)) → MARK.0(X2)
MARK.0(sel.0-1(sel.0-1(x0, x1), y1)) → ACTIVE.0(sel.0-0(active.0(sel.0-0(mark.0(x0), mark.1(x1))), mark.1(y1)))
ACTIVE.0(sel.0-0(s.0(X), cons.1-0(Y, Z))) → MARK.0(sel.0-0(X, Z))
ACTIVE.0(sel.0-0(s.0(X), cons.0-1(Y, Z))) → MARK.0(sel.0-1(X, Z))
MARK.0(sel.0-0(y0, cons.0-0(x0, x1))) → ACTIVE.0(sel.0-0(mark.0(y0), active.0(cons.0-0(mark.0(x0), x1))))
MARK.0(sel.1-0(0., y1)) → ACTIVE.0(sel.0-0(active.1(0.), mark.0(y1)))
MARK.0(s.0(X)) → MARK.0(X)
MARK.0(sel.1-0(y0, cons.1-1(x0, x1))) → ACTIVE.0(sel.0-0(mark.1(y0), active.0(cons.0-1(mark.1(x0), x1))))
MARK.0(g.0(cons.0-1(x0, x1))) → ACTIVE.0(g.0(active.0(cons.0-1(mark.0(x0), x1))))

The TRS R consists of the following rules:

sel.0-1(active.1(X1), X2) → sel.1-1(X1, X2)
mark.0(sel.1-1(X1, X2)) → active.0(sel.0-0(mark.1(X1), mark.1(X2)))
cons.1-0(X1, active.0(X2)) → cons.1-0(X1, X2)
mark.0(cons.1-1(X1, X2)) → active.0(cons.0-1(mark.1(X1), X2))
g.0(active.0(X)) → g.0(X)
cons.0-0(X1, active.1(X2)) → cons.0-1(X1, X2)
active.0(f.1(X)) → mark.0(cons.1-0(X, f.0(g.1(X))))
cons.0-1(active.0(X1), X2) → cons.0-1(X1, X2)
active.0(sel.0-0(s.0(X), cons.1-0(Y, Z))) → mark.0(sel.0-0(X, Z))
sel.1-0(X1, active.1(X2)) → sel.1-1(X1, X2)
cons.0-0(X1, mark.1(X2)) → cons.0-1(X1, X2)
sel.0-1(active.0(X1), X2) → sel.0-1(X1, X2)
cons.1-0(X1, active.1(X2)) → cons.1-1(X1, X2)
cons.0-0(active.0(X1), X2) → cons.0-0(X1, X2)
mark.0(cons.0-1(X1, X2)) → active.0(cons.0-1(mark.0(X1), X2))
mark.0(sel.0-0(X1, X2)) → active.0(sel.0-0(mark.0(X1), mark.0(X2)))
mark.0(s.0(X)) → active.0(s.0(mark.0(X)))
active.0(sel.0-0(s.1(X), cons.1-0(Y, Z))) → mark.0(sel.1-0(X, Z))
mark.0(f.1(X)) → active.0(f.0(mark.1(X)))
sel.0-0(mark.1(X1), X2) → sel.1-0(X1, X2)
sel.0-0(X1, mark.0(X2)) → sel.0-0(X1, X2)
cons.0-1(mark.0(X1), X2) → cons.0-1(X1, X2)
cons.0-0(X1, mark.0(X2)) → cons.0-0(X1, X2)
sel.0-0(X1, mark.1(X2)) → sel.0-1(X1, X2)
cons.0-0(active.1(X1), X2) → cons.1-0(X1, X2)
active.0(sel.0-0(s.1(X), cons.1-1(Y, Z))) → mark.0(sel.1-1(X, Z))
f.0(mark.0(X)) → f.0(X)
f.0(active.1(X)) → f.1(X)
g.0(mark.0(X)) → g.0(X)
cons.1-0(X1, mark.0(X2)) → cons.1-0(X1, X2)
active.0(g.0(s.1(X))) → mark.0(s.0(s.0(g.1(X))))
sel.0-1(mark.1(X1), X2) → sel.1-1(X1, X2)
active.0(sel.0-0(s.0(X), cons.0-1(Y, Z))) → mark.0(sel.0-1(X, Z))
cons.0-0(X1, active.0(X2)) → cons.0-0(X1, X2)
mark.0(s.1(X)) → active.0(s.0(mark.1(X)))
active.0(sel.1-0(0., cons.1-0(X, Y))) → mark.1(X)
mark.0(cons.0-0(X1, X2)) → active.0(cons.0-0(mark.0(X1), X2))
cons.1-0(X1, mark.1(X2)) → cons.1-1(X1, X2)
sel.0-1(mark.0(X1), X2) → sel.0-1(X1, X2)
mark.1(0.) → active.1(0.)
active.0(sel.0-0(s.1(X), cons.0-1(Y, Z))) → mark.0(sel.1-1(X, Z))
sel.1-0(X1, active.0(X2)) → sel.1-0(X1, X2)
active.0(g.0(s.0(X))) → mark.0(s.0(s.0(g.0(X))))
sel.0-0(active.0(X1), X2) → sel.0-0(X1, X2)
cons.0-1(mark.1(X1), X2) → cons.1-1(X1, X2)
sel.0-0(X1, active.0(X2)) → sel.0-0(X1, X2)
s.0(active.0(X)) → s.0(X)
sel.0-0(active.1(X1), X2) → sel.1-0(X1, X2)
cons.0-1(active.1(X1), X2) → cons.1-1(X1, X2)
mark.0(g.1(X)) → active.0(g.0(mark.1(X)))
f.0(active.0(X)) → f.0(X)
s.0(mark.1(X)) → s.1(X)
sel.0-0(mark.0(X1), X2) → sel.0-0(X1, X2)
active.0(sel.0-0(s.1(X), cons.0-0(Y, Z))) → mark.0(sel.1-0(X, Z))
active.0(sel.0-0(s.0(X), cons.0-0(Y, Z))) → mark.0(sel.0-0(X, Z))
sel.1-0(X1, mark.0(X2)) → sel.1-0(X1, X2)
active.0(sel.1-0(0., cons.0-0(X, Y))) → mark.0(X)
active.0(g.1(0.)) → mark.0(s.1(0.))
sel.0-0(X1, active.1(X2)) → sel.0-1(X1, X2)
g.0(active.1(X)) → g.1(X)
mark.0(sel.1-0(X1, X2)) → active.0(sel.0-0(mark.1(X1), mark.0(X2)))
s.0(active.1(X)) → s.1(X)
mark.0(f.0(X)) → active.0(f.0(mark.0(X)))
active.0(sel.0-0(s.0(X), cons.1-1(Y, Z))) → mark.0(sel.0-1(X, Z))
cons.0-0(mark.1(X1), X2) → cons.1-0(X1, X2)
sel.1-0(X1, mark.1(X2)) → sel.1-1(X1, X2)
mark.0(cons.1-0(X1, X2)) → active.0(cons.0-0(mark.1(X1), X2))
active.0(sel.1-0(0., cons.0-1(X, Y))) → mark.0(X)
mark.0(g.0(X)) → active.0(g.0(mark.0(X)))
g.0(mark.1(X)) → g.1(X)
s.0(mark.0(X)) → s.0(X)
f.0(mark.1(X)) → f.1(X)
active.0(f.0(X)) → mark.0(cons.0-0(X, f.0(g.0(X))))
active.0(sel.1-0(0., cons.1-1(X, Y))) → mark.1(X)
cons.0-0(mark.0(X1), X2) → cons.0-0(X1, X2)
mark.0(sel.0-1(X1, X2)) → active.0(sel.0-0(mark.0(X1), mark.1(X2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
As can be seen after transforming the QDP problem by semantic labelling [33] and then some rule deleting processors, only certain labelled rules and pairs can be used. Hence, we only have to consider all unlabelled pairs and rules (without the decreasing rules for quasi-models). 

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ SemLabProof
                        ↳ SemLabProof2
                          ↳ QDP
                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(sel(y0, f(x0))) → ACTIVE(sel(mark(y0), active(f(mark(x0)))))
MARK(s(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(mark(x0), x1)), mark(y1)))
MARK(g(X)) → MARK(X)
ACTIVE(f(X)) → MARK(cons(X, f(g(X))))
MARK(g(f(x0))) → ACTIVE(g(active(f(mark(x0)))))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(mark(x0), x1))))
MARK(g(cons(x0, x1))) → ACTIVE(g(active(cons(mark(x0), x1))))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(g(g(x0))) → ACTIVE(g(active(g(mark(x0)))))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(mark(x0)))))
MARK(f(X)) → MARK(X)
MARK(g(sel(x0, x1))) → ACTIVE(g(active(sel(mark(x0), mark(x1)))))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(sel(X1, X2)) → MARK(X1)
ACTIVE(g(s(X))) → MARK(s(s(g(X))))
MARK(sel(g(x0), y1)) → ACTIVE(sel(active(g(mark(x0))), mark(y1)))
MARK(sel(f(x0), y1)) → ACTIVE(sel(active(f(mark(x0))), mark(y1)))
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(g(s(x0))) → ACTIVE(g(active(s(mark(x0)))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(g(x0)) → ACTIVE(g(x0))
MARK(sel(y0, g(x0))) → ACTIVE(sel(mark(y0), active(g(mark(x0)))))
MARK(g(0)) → ACTIVE(g(active(0)))
MARK(sel(X1, X2)) → MARK(X2)
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(mark(x0))), mark(y1)))

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(g(0)) → ACTIVE(g(active(0))) at position [0] we obtained the following new rules:

MARK(g(0)) → ACTIVE(g(0))



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ SemLabProof
                        ↳ SemLabProof2
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(sel(y0, f(x0))) → ACTIVE(sel(mark(y0), active(f(mark(x0)))))
MARK(s(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(mark(x0), x1)), mark(y1)))
ACTIVE(f(X)) → MARK(cons(X, f(g(X))))
MARK(g(X)) → MARK(X)
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(g(f(x0))) → ACTIVE(g(active(f(mark(x0)))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(mark(x0), x1))))
MARK(g(cons(x0, x1))) → ACTIVE(g(active(cons(mark(x0), x1))))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(g(g(x0))) → ACTIVE(g(active(g(mark(x0)))))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
MARK(g(0)) → ACTIVE(g(0))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(mark(x0)))))
MARK(f(X)) → MARK(X)
MARK(g(sel(x0, x1))) → ACTIVE(g(active(sel(mark(x0), mark(x1)))))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
ACTIVE(g(s(X))) → MARK(s(s(g(X))))
MARK(sel(g(x0), y1)) → ACTIVE(sel(active(g(mark(x0))), mark(y1)))
MARK(sel(f(x0), y1)) → ACTIVE(sel(active(f(mark(x0))), mark(y1)))
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(g(s(x0))) → ACTIVE(g(active(s(mark(x0)))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, g(x0))) → ACTIVE(sel(mark(y0), active(g(mark(x0)))))
MARK(g(x0)) → ACTIVE(g(x0))
MARK(sel(X1, X2)) → MARK(X2)
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(mark(x0))), mark(y1)))

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ SemLabProof
                        ↳ SemLabProof2
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MARK(sel(y0, f(x0))) → ACTIVE(sel(mark(y0), active(f(mark(x0)))))
MARK(s(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(mark(x0), x1)), mark(y1)))
MARK(g(X)) → MARK(X)
ACTIVE(f(X)) → MARK(cons(X, f(g(X))))
MARK(g(f(x0))) → ACTIVE(g(active(f(mark(x0)))))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(mark(x0), x1))))
MARK(g(cons(x0, x1))) → ACTIVE(g(active(cons(mark(x0), x1))))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(g(g(x0))) → ACTIVE(g(active(g(mark(x0)))))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(mark(x0)))))
MARK(f(X)) → MARK(X)
MARK(g(sel(x0, x1))) → ACTIVE(g(active(sel(mark(x0), mark(x1)))))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
ACTIVE(g(s(X))) → MARK(s(s(g(X))))
MARK(sel(g(x0), y1)) → ACTIVE(sel(active(g(mark(x0))), mark(y1)))
MARK(sel(f(x0), y1)) → ACTIVE(sel(active(f(mark(x0))), mark(y1)))
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(g(s(x0))) → ACTIVE(g(active(s(mark(x0)))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, g(x0))) → ACTIVE(sel(mark(y0), active(g(mark(x0)))))
MARK(g(x0)) → ACTIVE(g(x0))
MARK(sel(X1, X2)) → MARK(X2)
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(mark(x0))), mark(y1)))

The TRS R consists of the following rules:

active(f(X)) → mark(cons(X, f(g(X))))
active(g(0)) → mark(s(0))
active(g(s(X))) → mark(s(s(g(X))))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
mark(f(X)) → active(f(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(g(X)) → active(g(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
g(mark(X)) → g(X)
g(active(X)) → g(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.